COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Since its inception, the Laboratory has devoted a certain amount
C00006 ENDMK
C⊗;
	Since its inception, the Laboratory has devoted a certain amount
of its effort to the problem of how to represent information in a
computer for artificial intelligence purposes.  The starting point of our
efforts  was (McCarthy 1959) which was the first paper to separate the
representation problem from the problem of heuristics and to propose that
languages of mathematical logic be used to represent declarative information.
Among other things, that paper proposed a program called the Advice Taker
that would be able to combine facts given to it about a particular program
with general information about the world and come up with a solution to
a problem.  Although it has been fifteen years since the Advice Taker was
first proposed, no-one at Stanford or elsewhere has been able to make a
system with the capabilities proposed although there have been a few
partial efforts.  This is mainly because the theoretical problems required
to do this have not been solved.  Some people think that this is because
the approach is mistaken, but we think the problem is just very difficult
and requires new ideas for its solution.

	At Stanford, McCarthy has worked on the problem intermittently
producing and AI Memo (McCarthy 1963) and a paper (McCarthy and Hayes 1969)
in the process.  Other efforts here included (Safier 1964) and (Sandewall
1971).  Sandewall has been active in this area in Sweden before and since.

	There are considerable connections between this work and the work in
mathematical theory of computation, the work in theorem proving, and the
work in natural language carried on in the Laboratory.  Namely, good axiom
systems for first order logic and corresponding proof checkers are required
for both mathematical theory of computation and formal reasoning in artificial
intelligence, and the theory of correctness of computer programs should
generalize to proving that strategies will achieve goals.  Theorem proving
programs have used as examples problems arising in representation theory.
The workers in natural language are only beginning to study what facts about
the world are expressed in the sentences they have been studying from a
syntactic point of view.